x1:Realizer. (Reffect?(x1))  (Reffect-loc(x1)  Id) 

latex

Definitions	if b then t else f fi , tt, ff, Reffect-loc(x1), t  T, Reffect?(x1), b, P  Q, x:A. B(x), False, Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, , Rnone(),
Lemmas	Reffect? wf, assert wf, true wf, false wf, es realizer wf